{-# LANGUAGE TypeFamilies, FlexibleContexts, TypeOperators,
  ScopedTypeVariables, UndecidableInstances, FlexibleInstances #-}

{-# LANGUAGE MultiParamTypeClasses, QuasiQuotes, GADTs #-}

{-# LANGUAGE TemplateHaskell #-}

{- |

Module      :  Type.Yoko.Type
Copyright   :  (c) The University of Kansas 2011
License     :  BSD3

Maintainer  :  nicolas.frisby@gmail.com
Stability   :  experimental
Portability :  see LANGUAGE pragmas (... GHC)

Some fundamental types central to @yoko@.

-}

module Type.Yoko.Type
  (qK, Proxy(Proxy), module Type.Yoko.Type, module Type.Yoko.Wrapper,
   module Type.Spine.Stage0, module Type.Booleans, module Type.Yoko.Maybe,
   IsEQ, Compare, EqT(..), (:=:)(..), EQ) where

import Data.Proxy (Proxy(..))

import Type.Spine
import Type.Spine.Stage0 (KS, KTSS)
import Type.Serialize

import Data.Proxy.TH (qProxy)
import Type.Booleans
--import Polarity
import Type.Ord.SpineSerialize (EQ, IsEQ, Compare)

import Data.Type.Equality

import Type.Yoko.Wrapper hiding (__varD)
import Type.Yoko.Maybe



qP = qProxy

-- | For use with proxy arguments that are to be inferred.
infP :: Proxy a
infP = Proxy



-- | The @Med@ type family encodes the behavior of recursion mediators.
type family Med m a
-- | @type instance Med IdM a = a@.
data IdM = IdM; type instance Med IdM a = a





derive n = do
  d <- spineType n
  (d ++) `fmap` serializeTypeAsHash n





-- | Composition of @* -> *@ types.
newtype (f :. g) a = Compose (f (g a)); wraps_thinly ''(:.)

-- | Explicitly takes the inner type as a proxy.
composeWith :: [qProxy|g :: *->*|] -> f (g a) -> (f :. g) a
composeWith _ = Compose
